X:Type, eq:EqDecider(X), f, g:x:X fp Type, x:X. f || g  (f(x)?Void r g(x)?Top) 

latex

Definitions	x:A. B(x), P  Q, f(x)?z, Top, t  T, if b then t else f fi , x. t(x), tt, ff, , P & Q, , x(s), Unit, P  Q, f || g,
Lemmas	fpf-dom wf, fpf-trivial-subtype-top, bool wf, eqtt to assert, fpf-ap wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-cap wf, top wf, fpf-compatible wf, fpf wf, deq wf